es:ES, as, bs:E List.
loc-ordered(es;as)  loc-ordered(es;bs)  (as = bs  (e:E. (e  as)  (e  bs))) 

latex

Definitions	t  T, x:A. B(x), Void, x:AB(x), P  Q, False, A, x.A(x), ES, type List, loc-ordered(es;L), s = t, (x  l), P  Q, (e <loc e'), x,y. t(x;y), E, Trans x,y:T. E(x;y), x:AB(x), P & Q
Lemmas	es-axioms, event system wf, l-ordered-equality, es-locl-antireflexive, es-locl wf, es-E wf